\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $e$:es{-}E(${\it es}$), $l$:IdLnk, $L$:(es{-}E(${\it es}$) List).
\\[0ex]es{-}rcv{-}from(${\it es}$; $e$; $l$; $L$)
\\[0ex]$\Rightarrow$ \=($\forall$$i$:int\_seg(0; $\parallel$$L$$\parallel$). \+
\\[0ex]$\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex](($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; ${\it e'}$) = $l$)
\\[0ex]$\wedge$ (es{-}sender(${\it es}$; ${\it e'}$) = $e$)
\\[0ex]$\wedge$ (es{-}index(${\it es}$; ${\it e'}$) = $i$ $\in$ $\mathbb{Z}$)))
\-\-
\end{tabbing}